Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

incr(nil) → nil
incr(cons(X, L)) → cons(s(X), incr(L))
adx(nil) → nil
adx(cons(X, L)) → incr(cons(X, adx(L)))
nats → adx(zeros)
zeros → cons(0, zeros)
head(cons(X, L)) → X
tail(cons(X, L)) → L

The replacement map contains the following entries:

incr: {1}
nil: empty set
cons: {1}
s: {1}
adx: {1}
nats: empty set
zeros: empty set
0: empty set
head: {1}
tail: {1}


↳ CSR
  ↳ CSRInnermostProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

incr(nil) → nil
incr(cons(X, L)) → cons(s(X), incr(L))
adx(nil) → nil
adx(cons(X, L)) → incr(cons(X, adx(L)))
nats → adx(zeros)
zeros → cons(0, zeros)
head(cons(X, L)) → X
tail(cons(X, L)) → L

The replacement map contains the following entries:

incr: {1}
nil: empty set
cons: {1}
s: {1}
adx: {1}
nats: empty set
zeros: empty set
0: empty set
head: {1}
tail: {1}

The CSR is orthogonal. By [10] we can switch to innermost.

↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

incr(nil) → nil
incr(cons(X, L)) → cons(s(X), incr(L))
adx(nil) → nil
adx(cons(X, L)) → incr(cons(X, adx(L)))
nats → adx(zeros)
zeros → cons(0, zeros)
head(cons(X, L)) → X
tail(cons(X, L)) → L

The replacement map contains the following entries:

incr: {1}
nil: empty set
cons: {1}
s: {1}
adx: {1}
nats: empty set
zeros: empty set
0: empty set
head: {1}
tail: {1}

Innermost Strategy.

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {incr, s, adx, head, tail, INCR, ADX, TAIL} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

ADX(cons(X, L)) → INCR(cons(X, adx(L)))
NATS → ADX(zeros)
NATS → ZEROS

The collapsing dependency pairs are DPc:

TAIL(cons(X, L)) → L


The hidden terms of R are:

incr(L)
zeros

Every hiding context is built from:

incr on positions {1}
adx on positions {1}

Hence, the new unhiding pairs DPu are :

TAIL(cons(X, L)) → U(L)
U(incr(x_0)) → U(x_0)
U(adx(x_0)) → U(x_0)
U(incr(L)) → INCR(L)
U(zeros) → ZEROS

The TRS R consists of the following rules:

incr(nil) → nil
incr(cons(X, L)) → cons(s(X), incr(L))
adx(nil) → nil
adx(cons(X, L)) → incr(cons(X, adx(L)))
nats → adx(zeros)
zeros → cons(0, zeros)
head(cons(X, L)) → X
tail(cons(X, L)) → L

The set Q consists of the following terms:

incr(nil)
incr(cons(x0, x1))
adx(nil)
adx(cons(x0, x1))
nats
zeros
head(cons(x0, x1))
tail(cons(x0, x1))


The approximation of the Context-Sensitive Dependency Graph contains 1 SCC with 5 less nodes.


↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof
            ↳ QCSDP
              ↳ QCSDPSubtermProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {incr, s, adx, head, tail} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.

The TRS P consists of the following rules:

U(incr(x_0)) → U(x_0)
U(adx(x_0)) → U(x_0)

The TRS R consists of the following rules:

incr(nil) → nil
incr(cons(X, L)) → cons(s(X), incr(L))
adx(nil) → nil
adx(cons(X, L)) → incr(cons(X, adx(L)))
nats → adx(zeros)
zeros → cons(0, zeros)
head(cons(X, L)) → X
tail(cons(X, L)) → L

The set Q consists of the following terms:

incr(nil)
incr(cons(x0, x1))
adx(nil)
adx(cons(x0, x1))
nats
zeros
head(cons(x0, x1))
tail(cons(x0, x1))


We use the subterm processor [20].


The following pairs can be oriented strictly and are deleted.


U(incr(x_0)) → U(x_0)
U(adx(x_0)) → U(x_0)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
U(x1)  =  x1

Subterm Order


↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof
            ↳ QCSDP
              ↳ QCSDPSubtermProof
                ↳ QCSDP
                  ↳ PIsEmptyProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {incr, s, adx, head, tail} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

incr(nil) → nil
incr(cons(X, L)) → cons(s(X), incr(L))
adx(nil) → nil
adx(cons(X, L)) → incr(cons(X, adx(L)))
nats → adx(zeros)
zeros → cons(0, zeros)
head(cons(X, L)) → X
tail(cons(X, L)) → L

The set Q consists of the following terms:

incr(nil)
incr(cons(x0, x1))
adx(nil)
adx(cons(x0, x1))
nats
zeros
head(cons(x0, x1))
tail(cons(x0, x1))


The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.